T:Type, R:(TT). R!^+ => R^+ 

latex

Definitions	R!, R^+, R1 => R2, x f y, , Type, P  Q, A, P & Q, , x:A  B(x), x:A. B(x), f(a), rel_exp(T;R;n), x:A. B(x), x:AB(x), t  T, Dec(P), P  Q, s ~ t, SQType(T), {T}, #$n, left + right, Unit, P  Q, (i = j), , b, s = t, b, x.A(x), , {x:A| B(x)} , Void, A  B, , A c B, False, a < b, n - m, n+m, -n
Lemmas	le wf, not wf, assert wf, bnot wf, bool wf, eq int wf, assert of eq int, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, decidable int equal, nat plus properties, nat plus inc, rel exp wf